Collection of Internet/Collection of Internet.iso/faq/comp/meta_lan

Text File | 1994-03-17 | 38KB | 936 lines

Newsgroups: comp.lang.ml,comp.answers,news.answers
Path: bloom-beacon.mit.edu!hookup!news.moneng.mei.com!howland.reston.ans.net!europa.eng.gtefsd.com!fs7.ece.cmu.edu!honeydew.srv.cs.cmu.edu!jgmorris
From: [e-mail] (Greg Morrisett)
Subject: Comp.Lang.ML FAQ [Monthly Posting]
Message-ID: <[e-mail]>
Followup-To: poster
Summary: This posting contains a list of Frequently asked questions (and their
         answers) about the family of ML programming languages, including
         Standard ML, CAML, Lazy-ML, and CAML-Light.  This post should be read
         before asking a question on the comp.lang.ml newsgroup.
Originator: [e-mail]
Sender: [e-mail]
Nntp-Posting-Host: vache.venari.cs.cmu.edu
Reply-To: [e-mail]
Organization: School of Computer Science, Carnegie Mellon
Date: Thu, 17 Mar 1994 17:03:58 GMT
Approved: [e-mail]
Expires: Sun, 17 Apr 1994 00:00:00 GMT
Lines: 914
Xref: bloom-beacon.mit.edu comp.lang.ml:404 comp.answers:4201 news.answers:16492

Archive-name: meta-lang-faq
Last-modified: 1994/01/11


         COMP.LANG.ML Frequently Asked Questions and Answers
       (compiled by Dave Berry and Greg Morrisett)

Please send corrections, additions, or comments regarding this list to
[e-mail].

Changes since last month:
------------------------
1. Added info on emacs mode
2. The NJ library is now (and has been) version 0.2

Contents:
---------
    1. What is ML?
    2. Where is ML discussed?
        a. Comp.Lang.ML
        b. SML-LIST
        c. CAML-LIST
    3. What implementations of ML are available?
        a. quick summary (by machine/OS)
        b. Poly/ML
        c. Standard ML of New Jersey
        d. Poplog ML
        e. ANU ML
        f. MicroML
        g. sml2c
        h. Caml Light
        i. ML Kit Compiler
    4. Unsupported SML/NJ Ports
        a. MS-DOS/Windows
        b. Linux
        c. OS/2
        5. Where can I find documentation on ML?
        a. The Definition
        b. Textbooks
    6. Where can I find ML library code?
    7. Theorem Provers and ML
        8. Miscellaneous Questions
        a. How do I write the Y combinator in SML?
        b. Where can I find an X-windows interface to SML?
        c. How do I call a C function from SML/NJ?
        d. How do I fix the emacs mode to work with
            emacs 19?

--------------------------------------------------------------------------
1. What is ML?

  ML (which stands for Meta-Language) is a family of advanced programming
  languages with [usually] functional control structures, strict semantics,
  a strict polymorphic type system, and parametrized modules.  It includes
  Standard ML, Lazy ML, CAML, CAML Light, and various research languages.
  Implementations are available on many platforms, including PCs, mainframes,
  most models of workstation, multi-processors and supercomputers.  ML has
  many thousands of users, is taught at many universities (and is the first
  programming language taught at some).

--------------------------------------------------------------------------
2. Where is ML discussed?

COMP.LANG.ML
------------
comp.lang.ml is a moderated usenet newsgroup.  The topics for discussion
include but are not limited to:

   * general ML enquiries or discussion
   * general interpretation of the definition of Standard ML
   * applications and use of ML
   * announcements of general interest (e.g. compiler releases)
   * discussion of semantics including sematics of extensions based on ML
   * discussion about library structure and content
   * tool development
   * comparison/contrast with other languages
   * implementation issues, techniques and algorithms including extensions
       based on ML

Requests should be sent to:

    [e-mail]

Administrative mail should be sent to:

    [e-mail]

Messages sent to the newsgroup are archived at CMU.  The archives can be
retrieved by anonymous ftp from internet sites.  Messages are archived
on a year-to-year basis.  Previous years' messages are compressed using
the Unix "compress" command.  The current year's messages are not
compressed.

    ftp pop.cs.cmu.edu
    username: anonymous
    password: <username>@<site>
    binary
    cd /usr/jgmorris/sml-archive
    get sml-archive.<year>.Z
    quit
    zcat sml-archive.<year>.Z

(Pop's IP address is 128.2.205.205).

Individual messages can also be accessed in the directories
/usr/jgmorris/mh-sml-archive/<year>-sml.

SML-LIST
--------
The SML-LIST is a mailing list that exists for people who cannot
(or do not want to) read the Usenet COMP.LANG.ML newsgroup.
Messages are crossposted from COMP.LANG.ML to the SML-LIST and
vice-versa.  You should ask to join the SML-LIST _only if_ you cannot
(or do not want to) read the Usenet COMP.LANG.ML newsgroup.

To send a message to the SML-LIST distribution, address it to:

    [e-mail]

(sites not connected to the Internet may need additional routing.)

Administrative mail such as requests to add or remove names from the
distribution list should be addressed to

    [e-mail]


CAML-LIST
---------
The Caml language, a dialect of ML, is discussed on the Caml mailing
list.  To send mail to the Caml mailing list, address it to:

    [e-mail]

Administrative mail should be addressed to:

    [e-mail]

ALT.LANG.ML
-----------
Another venue for ML-related discussion is the Netnews group
alt.lang.ml, though this has seen relatively little traffic.
--------------------------------------------------------------------------
3. What implementations of ML are available and where can I find them?
   (Note, this information may be out of date.)

Quick Summary:

System    full SML?  contact                        Platforms
------    ---------  ------------                 ------------------------------
Poly/ML       yes       [e-mail]                Unix/Sparc,Sun3 (others soon)

SML/NJ       yes     [e-mail]             Unix/Sparc,Mips,Vax,680x0,
           ftp research.att.com             I386/486,HPPA,RS/6000,
                         MacOS/MacII
           ftp.rz.uni-karlsruhe.de     Linux (including binaries)
           ftp-os2.nmsu.edu         OS/2  (including binearies)


PoplogML   yes       [e-mail],             VMS/Vax, Unix/Vax,Suns,Sparcs,
           [e-mail],       Solbourne, Sequent Symmetry,
           [e-mail]             HP M680?0, Apollo, AUX/MacII

Edinburgh  core       ftp ftp.dcs.ed.ac.uk             32-bit machines (bytecode)
           ftp ftp.informatik.uni-muenchen.de PC 80386SX+

ANU ML       core    [e-mail]     Sun-3, Ultrix/Vax, Pyramid,
                         AUX/MacII

MicroML       core    olof or mahler @cs.umu.se     PC 80286+ (bytecode)
           ftp ftp.cs.umu.se

sml2c       yes       [e-mail]         32-bit Unix machines (C code)
           ftp dravido.soar.cs.cmu.edu

Caml Light coreish [e-mail]     32-bit Unix, Mac, PC 8086,
           ftp ftp.inria.fr         PC 80386 (bytecode)

Kit       yes       ftp ftp.diku.dk         (Requires another SML compiler
           ftp ftp.dcs.ed.ac.uk          to build binaries)

Details:

Poly/ML:
    Poly/ML produces native code for SPARC and Sun3
systems.  Poly/ML uses a persistent store and supports arbitrary precision
integer arithmetic.  It comes with a make system, an X11/Xlib interface,
and a OSF/Motif interface.  Non-standard extensions include concurrent
processes and an associated message-passing scheme.
    Poly/ML is distributed by Abstract Hardware Ltd. ([e-mail]).
The price of the Motif edition is 1250 pounds for an academic site
licence or 3300 pounds per machine for commercial users.  Multiple
and site licences are available by negotiation.

Standard ML of New Jersey:
        Standard ML of New Jersey was developed jointly at AT&T Bell
Laboratories and Princeton University.  It is an open system (source
code is freely available) implemented in Standard ML.  Version 0.93 of
SML/NJ generates native code for 68020, SPARC, and MIPS (big and
little endian), I386/486, HPPA(HP9000/700), and RS/6000 architectures
under various versions of the Unix operating system (SunOS, Ultrix,
Mach, Irix, Riscos, HPUX, AIX, AUX, etc.), and on the MacIntosh OS
(Mac II, System 7.x, min 12MB ram).  Version 0.75 runs on the Vax
under Ultrix, BSD, and Mach.
    SML/NJ comes with a source-level debugger, profiler, gnu emacs
interface, ML implementations of LEX, YACC, and Twig, separate compilation
facilities, Concurrent ML, the eXene X Window library, and the SML/NJ
library.  It runs interactively and can produce stand-alone executable
applications.
    Non-standard extensions include typed first-class continuations,
Unix signal handling, and higher-order functors.
        SML/NJ is copyrighted by AT&T but the system, including source
code, is freely distributable.  It is available by anonymous ftp from
research.att.com (192.20.225.2) and princeton.edu (128.112.128.1).
Login as "anonymous" with your user name as password.  Put ftp in
binary mode and copy the (compressed tar) files you need from the
directory dist/ml (pub/ml on princeton.edu).  You only need the 93.mo.*.tar.Z
files for your machine in addition to the 93.src.tar.Z.  (You might also
want the 93.release-notes.[ps|txt], 93.tools.tar.Z, 93.doc.tar.Z, and
smlnj-lib-0.2.tar.Z files.)  Alternatively mail [e-mail].
In the UK, SML/NJ is available from the LFCS.
    There are unsupported ports of SML/NJ to other platforms, including
Linux, FreeBSD, OS/2, and Microsoft Windows 3.1.  See the "Unsupported SML/NJ
Ports" section for details.

Poplog ML:
        Standard ML is supported as part of the Poplog system, which also
provides incremental compilers for Pop-11, Common Lisp and Prolog in a
common environment with shared data-structures, so that mixed language
programming is possible. The integrated editor and HELP mechanism
support online teaching aids.  Poplog comes with an X Windows interface.
    Poplog is available for VAX+VMS, VAX+Ultrix, VAX+Bsd 4.2/3,
Sun-2,3,4, Sun386i, SPARCstation, Solbourne, Sequent Symmetry (with Dynix),
HP M680?0+Unix workstations and Apollo+Unix. Versions for MAC-II with A/UX,
DECstation 3100 and MIPS will be available shortly.
        UK educational users should contact the School of Cognitive and
Computing Sciences, University of Sussex ([e-mail]).  People in
the USA or Canada should contact Computable Functions Inc. ([e-mail]).
All others should contact Integral Solutions Ltd. ([e-mail]).  UK
academic prices start at 600 pounds.  Non-UK academic prices start at 1125
pounds.  Commercial prices start around 2,000 pounds for an ML-only version
or 7,500 pounds for the full Poplog system.

Edinburgh ML 4.0:
    Edinburgh ML 4.0 is an implementation of the core language (without
the module system).  It uses a bytecode interpreter, which is written in C
and runs on any machine with 32 bit words, a continuous address space and
a correct C compiler.  Ports to various 16 bit machines are underway.  The
bytecode interpreter can be compiled with switches to avoid the buggy parts
of the C compilers that we've used it with (as far as I know none of them
worked correctly).
    Edinburgh ML 4.0 is available from the LFCS.
    A port to PCs with 386SX processors or better is available by FTP
from ftp.informatik.uni-muenchen.de, in the file pub/sml/ibmpc/edml3864.exe.
Contact Joern Erbguth ([e-mail]) for more
information.
    Some information from Felix von Normann follows:

    There are other Edinburgh (PC-)ports of ML including an OS/2 2.x,
    an OS/2 PM and a Dos version. A new version has just been made
    ready and is available at forwiss.uni-passau.de (132.231.1.10) in
    pub/ibmpc/os2/lang/sml/sml04.zip. It is about 360K long (short?).

    All 3 programs have in common (all in one .zip):
       - true 32 Bit applications
       - easy to install, easy to use
       - As far as I know they work stable
         (except the DOS version working as a Windows window
         [you can use it with Windows but it crashes on *exit*])
       - they don't require expensive hardware
         (and they don't need a co-processor)

    To be more specific:
          OS/2 PM               OS/2                DOS
    OS    >= OS/2 2.0+ServPak   >= OS/2 2.0        >= DOS 5.0
    Edit  PM, GUI,              Standard            command history
          integrated editor
          (cut&paste)
    HW    >= 386/33, 8MB        >= 386/33 4MB       >= 386sx, 2MB
          lots of MB and fast
          graphics ad. recommened
    Help  online                online
          (+ML ref. in german)

ANU ML
    ANU ML is descended from Cardelli's ML Pose 3.  It implements the
core language of the standard and an old version of modules.  It incrementally
compiles to native code on Sun-3, Vax/Ultrix, Pyramid and MacII/AUX.  (It
is intended to standardize modules and do the port to Sun-4 in the near
future.)
    ANU ML has a program development system with strong support for
debugging (tracing, automatic retesting etc.) and has been extended with
a built-in type complex.
    ANU ML is still considered to be in beta release since exceptions
have been standardized quite recently.  It is available from Malcolm Newey,
CS Dept., Australian National University ([e-mail]) by
arrangement; soon to be available by ftp.

MicroML
    MicroML is an interpreter for a subset of SML that runs on IBM PCs,
from the Institute of Information Processing at the University of Umea in
Sweden.  It implements the core language except for records.  A 80286
processor or better is recommended.
    MicroML is available as an alpha-release by anonymous ftp from
ftp.cs.umu.se /pub/umlexe01.uue.  There are several known bugs in the current
version.  For more information contact Olof Johansson ([e-mail]) or
Roger Mahler ([e-mail]).

sml2c
    sml2c is a Standard ML to C compiler.  It is based on SML/NJ and
shares its front-end and most of the runtime system. sml2c is a batch
compiler and compiles only module-level declarations.  It does not support
SML/NJ style debugging and profiling.
    sml2c is easily portable and has been ported to IBM RT,
Decstation 3100, Decstation 5000, Omron Luna 88k, sun-3, sun-4 and a
486-based machine (running Mach).  The generated code is highly portable
and makes very few assumptions about the target machine or the C compilers
available on the target machine. The runtime system, which it shares with
the SML/NJ has several machine and operating system dependencies.  sml2c
has eliminated some of these dependencies by using portable schemes for
garbage collection and for freezing and restarting programs.
    sml2c is available by anonymous ftp from dravido.soar.cs.cmu.edu
(128.2.220.26). Log in as anonymous, send username@node as password.  The
compressed tar file sml2c.tar.Z can be found in /usr/nemo/sml2c.  The local
ftp software will allow you to change directory only to /usr/nemo/sml2c.
The size of the tar file is about 3 Meg. The size of the uncompressed
distribution is about 12 Meg.

Caml Light

Caml Light is a portable, bytecode interpreter for a subset of CAML,
a dialect of ML.  Some features of Caml Light include separate compilation,
streams and stream parsers, ability to link to C code, and tools for
building libraries and toplevel systems.  The PC versions provide
line editing and the 80386 port is VCPI-compliant.

The Unix version should work on any modern workstation. We have tested
it on Sun 3 and 4, DecStations, HP 9000/700 and 9000/350, IBM RS/6000,
SGI Indigo, Sony News, Next cubes, and some more exotic machines.
The Macintosh version is now a standalone Macintosh application, and
no longer requires the Macintosh Programmer's Workshop. (Well, at
least for the toplevel environment; the batch compilers still run
under MPW.) The application provides some graphics primitives.
The PC version still comes in two flavors, one that run on any PC, but
is severely limited by the 640K barrier, and one that run on 80386 or
80486 PC's in 32 bit protected mode to circumvent these limitations.
Both versions now provide the same graphics primitives as the
Macintosh version.  Ports to OS/2 and to the Amiga are in progress.

The version 0.6 of the Caml Light system has been released, and is
available by anonymous FTP from:

        host:      ftp.inria.fr (192.93.2.54)

        directory: lang/caml-light

    Summary of the files:

        README                  More detailed summary
        cl6unix.tar.Z           Unix version
        cl6macbin.sea.hqx       Binaries for the Macintosh version
        cl6macsrc.sea.hqx       Source code for the Macintosh version
        cl6pc386bin.zip         Binaries for the 80386 PC version
        cl6pc386src.zip         Source code for the 80386 PC version
        cl6pc86bin.zip          Binaries for the 8086 PC version
        cl6pc86src.zip          Source code for the 8086 PC version
        cl6refman.*             Reference manual, in various formats
        cl6tutorial.*           Tutorial, in various formats

This release is mostly a bug-fix release and should be compatible with
Caml Light 0.5. The main changes are:

* Better handling of type abbreviations.

* Debugging mode (option -g to camlc and camllight) to get access
  to the internals of module implementations.

* New library modules:
    genlex    generic lexical analyser
    set       applicative sets over ordered types
    map       applicative maps over ordered types
    baltree   balanced binary trees over ordered types

* "compile" command at toplevel (especially useful in the Macintosh version).

* New contributed libraries and tools:
    camlmode    Emacs editing mode for Caml Light
    mletags     Indexing of Caml Light source files for use with Emacs "tags"
    search_isos Search libraries by types (modulo isomorphisms)
    libgraph    X implementation of the portable graphics library
    libnum      Arbitrary-precision arithmetic
    libstr      String operations, regular expressions

* The 80386 PC version is now DPMI-compliant, hence it can run under Windows
  (in text mode inside a DOS windows and with no graphics, though).

* More examples, including those from the book "Le langage Caml".

General questions and comments of interest to the Caml community
should be sent to [e-mail], the Caml mailing list.
(see question 3 above for details.)

ML Kit Compiler

  The ML Kit is a straight translation of the Definition of Standard
ML into a collection of Standard ML modules.  For example, every
inference rule in the Definition is translated into a small piece of
Standard ML code which implements it. The translation has been done
with as little originality as possible - even variable conventions
from the Definition are carried straight over to the Kit.

  If you are primarily interested in executing Standard ML programs
efficiently, the ML Kit is not the system for you! (It uses a lot of
space and is very slow.) The Kit is intended as a tool box for those
people in the programming language community who may want a
self-contained parser or type checker for full Standard ML but do not
want to understand the clever bits of a high-performance compiler. We
have tried to write simple code and module interfaces; we have not
paid any attention to efficiency.

  The documentation is around 100 pages long and is provided with the
Kit. It explains how to build, run, read and modify the Kit. It also
describes how typing of flexible records and overloading are handled
in the Kit.

  The ML Kit is written by Nick Rothwell, David N. Turner, Mads Tofte
and Lars Birkedal at Edinburgh and Copenhagen Universities.

  The ML Kit is available via anonymous ftp. Here is a sample dialog:

  ftp ftp.diku.dk              ftp ftp.dcs.ed.ac.uk
  Name: anonymous              Name: anonymous
  Password: <your loginname@host>      Password: <your loginname@host>
  ftp> binary                  ftp> binary
  ftp> cd diku/users/birkedal          ftp> cd export/ml/mlkit
  ftp> get README              ftp> get README
  ftp> get COPYING              ftp> get COPYING
  ftp> get src.tar.Z              ftp> get src.tar.Z
  ftp> get doc.tar.Z              ftp> get doc.tar.Z
  ftp> get tools.tar.Z          ftp> get tools.tar.Z
  ftp> get examples.tar.Z          ftp> get examples.tar.Z
  ftp> bye                  ftp> bye

The file README contains installation instructions. Note that no
binaries are distributed and that you must build these using either
Standard ML of New Jersey, or Poly/ML.


--------------------------------------------------------------------------
6. Unsupported SML/NJ Ports

This section describes various ports of SML/NJ (see section 5)
that are not directly supported by the NJ folks.

MS-DOS/Windows?
---------------
(From Dave MacQueen)

There is an MS-Windows/MSDOS implementation of Standard ML of New
Jersey available by annonymous ftp on research.att.com, directory
dist/ml/working/sml-386.  This port was done by Yngvi Guttesen at the
Danish Technical University in Copenhagen, and it is based on version
0.75 of SML/NJ.  The distribution consists of the following four
files.

-rw-rw-r--  1  dbm     other    417 Feb 16  1993 README
-rw-rw-r--  1  dbm     other  51375 Feb  7  1992 doc.tar.Z
-rw-rw-r--  1  dbm     other 749105 May  5  1992 mo.386.tar.Z
-rw-rw-r--  1  dbm     other 851445 Feb  7  1992 src.tar.Z

This Windows port is rather delicate, and when we got it we had a lot
of trouble getting it working here at Bell labs.  We tried several
different machines and finally found one on which it would run (a
Gateway 2000 with 16 MB of RAM), though even then it was not very
robust or fast.  It seemed to be a problem of finding a machine with
just the right memory management configuration.  I must admit that
memory management under Windows is a black art that I am not familiar
with, so I have no idea how to characterize the required memory
configuration.

My conclusion is that the current Windows 3.1/MSDOS environment is so
difficult that it would require a major additional investment to have
a really useful port.  Guttesen did not have a 32 bit C compiler
available, so he rewrote the runtime system in assember, which makes
it difficult to modify his port.  An alternative is to wait for
Windows NT (Win32) or OS/2 ports, which may be done in the coming
months (a couple of people have independently been working on OS/2
ports recently).  Another alternative is to look in directory pub/ml
of ftp.dcs.ed.ac.uk, where there are a couple of (partial)
implementations of SML that run on PCs.  A third alternative is to
look into Xavier Leroy's CAML Light.  (Details of these are in the
comp.lang.ml FAQ message.)

However, Guttesen's 386 code generator was used by Mark Leone of CMU
as the basis for a port to Unix on Ix86 machines.  The current release
of SML of New Jersey (0.93) incorporates Intel/Unix support for Mach
(used at Carnegie-Mellon University), BSD386 (a product of BSDI?), and
386bsd (a free version of Unix for the PC).  There are also versions
that run under Linux (available as part of the free Linux distribution)
and SVR4, although we have not yet integrated the code supporting
Linux and SVR4 into the distributed 0.93 runtime system.  Interest has
been expressed in a port for SCO Unix, but, as far as we know, no one
has done such a port.

Very recently Peter Bertelsen of the Technical University of Denmark
has done a port to OS2, which is now available on research.att.com,
directory dist/ml.

Linux?
------
(Thanks to Ralf Reetz, Peter Su, and Mark Leone)

Various ftp sites that seem to carry SML/NJ version 0.93 for Linux:

    ftp.rz.uni-karlsruhe.de:/linux/mirror.tsx/

        binaries/usr.bin/njsml.93.bin.z
        sources/usr.bin/njsml.93.linux.README
        sources/usr.bin/njsml.93.linux.README.NEW
        sources/usr.bin/njsml.93.linux.diffs.z
        sources/usr.bin/njsml.93.src.tar.z

    [e-mail]:/pub/linux/

           sources/usr.bin/njsml.93.src.tar.z

    ftp.dcs.glasgow.ac.uk?

From the README file:

             Standard ML of New Jersey
    Version 0.93 for the i386/i486 running Linux, April 23, 1993


__ WHAT
    SML/NJ is a compiler for the functional programming language
    Standard ML (SML). It is a fairly complete and robust
    implementation of ML.

__ FILES
    njsml.93.bin.z - gzip'd binary of njsml (no SourceGroup)
    njsml-sg.93.bin.z - gzip'd binary of njsml with SourceGroup
    njsml.93.src.tar.z - minimal sources for NJSML on Linux
    njsml.93.mo.i386.z - you'll need these also to compile on Linux

    You can pick up additional tools and goodies from:

    research.att.com

    under the "ml" directory.

__ HISTORY

    This is a port of Standard ML of New Jersey (SML/NJ) to Linux. It
    is based on the work of Mark Leone ([e-mail]) who did
    the port for i386/i486 machines. The current binary was compiled
    using Linux 0.99.7a.  Shared lib 4.3.3.

    This port was done by Sanford Barr ([e-mail]) based on
        the original port of 0.91 by Hermano Moura ([e-mail])
    and Andre Santos ([e-mail]).

__ RECOMMENDED ENV

    16M of ram is suggested if you wish to do anything serious with
    the system.  Also, a 386-40 or better would be helpful.


__ KNOWN BUGS AND DEFICIENCIES

    1 Some minimal precision problems exist when a 387 emulator is
      used.

    2 ML functions System.Directory.listDir and System.Directory.getWD
      not working at the moment.

__ WHERE

    NJ-SML 0.93 should be available at most major Linux sites.  It
    should also be available in:
        sbcs.sunysb.edu:/pub/linux
    by the time you are reading this.

OS/2:
-----
Standard ML of New Jersey (version 0.93) has been ported to PC's running OS/2.
Signal handling is not implemented. This port has been implemented using Mark
Leone's code generator for Intel 80386 and the Unix emulator emx, copyright of
Eberhard Mattes. SML/NJ is copyright of AT&T Bell Laboratories.
There is no warranty of any kind!

Requirements:
 - IBM OS/2 version 2.x
 - HPFS file system (long file names required)
 - emx version 0.8g or later
 - '.mo' files for i386

The port is available for anonymous ftp from research.att.com (in /dist/ml)
and, in Europe, from ftp.id.dth.dk (in /pub/bertelsen):

   93.os2port.zip     Archived with Info-ZIP's Zip utility
   93.os2port.tar.Z   Archived with GNU's tape archive utility
   93.os2port.txt     Port announcement & installation guide

Please note that the .tar.Z and .zip version of the SML/NJ port are exactly
alike and both contain a full source set (but no '.mo' files) for compiling
to OS/2 with emx/gcc (not included).

The i386 '.mo' archive (93.mo.i386.tar.Z) is available from research.att.com
(in /dist/ml) and princeton.edu (in /pub/ml). The emx environment is available
from various OS/2 related ftp sites, e.g. ftp-os2.cdrom.com.

A binary-only release of this SML/NJ port (no source, interactive system
executable only) is also available for anonymous ftp from ftp-os2.cdrom.com.

If you have questions concerning this port, please send email to:

Peter Bertelsen  ([e-mail])
Department of Computer Science, Technical University of Denmark

FreeBSD:
--------
SML/NJ is also available in source and binary format for FreeBSD from
freebsd.cdrom.com:/pub/FreeBSD/packages/sml_src.tgz and sml_bin.tgz.
The binary package includes EXene and CML as well.

--------------------------------------------------------------------------
5. Where can I find documentation on SML?

THE DEFINITION.

Robin Milner, Mads Tofte and Robert Harper
The Definition of Standard ML
MIT, 1990.
ISBN: 0-262-63132-6

Robin Milner and Mads Tofte
Commentary on Standard ML
MIT, 1991
ISBN: 0-262-63137-7

TEXTS.

Jeffrey D. Ullman
Elements of ML Programming
Prentice-Hall, 1993 (Oct. 15)
ISBN: 0-13-184854-2
(See Comp.Lang.ML archives, message from Ullman dated 22 Sep 1993 for
 chapter headings.)

Rachel Harrison
Abstract Data Types in Standard ML
John Wiley & Sons, April 1993
ISBN: 0-471-938440

Ake Wikstrom
Functional Programming Using Standard ML
Prentice Hall 1987
ISBN: 0-13-331661-0

Chris Reade
Elements of Functional Programming
Addison-Wesley 1989
ISBN: 0-201-12915-9

Lawrence C Paulson
ML for the Working Programmer
Cambridge University Press 1991
ISBN: 0-521-39022-2

Stefan Sokolowski
Applicative High Order Programming: The Standard ML perspective
Chapman & Hall 1991
ISBN: 0-412-39240-2     0-442-30838-8 (USA)

Ryan Stansifer
ML Primer
Prentice Hall, 1992
ISBN 0-13-561721-9

Colin Myers, Chris Clack, and Ellen Poon
Programming with Standard ML
Prentice Hall, 1993
ISBN 0-13-722075-8 (301pp)

The following report is available from the LFCS (Lorraine Edgar,
[e-mail]) and costs 5 pounds or 10 US dollars.  It covers all of
Standard ML.  The report is also available via the World Wide Web off of
http://www.cs.cmu.edu:8001/afs/cs.cmu.edu/project/fox/mosaic/HomePage.html.
Alternatively, the report can be ftp'd from ftp.cs.cmu.edu as the file
/afs/cs/project/fox/mosaic/intro-notes.ps.

Robert Harper
Introduction to Standard ML
LFCS Report Series  ECS-LFCS-86-14
Laboratory for Foundations of Computer Science
Department of Computer Science
University of Edinburgh
Nov. 1986 (revised Jan. 1989 by Nick Rothwell and Kevin Mitchell)

The following report is available from the LFCS (Lorraine Edgar,
[e-mail]) and costs 2.50 pounds or 5 US dollars for single
copies and 1.50 pounds or 3 dollars when bought in bulk.  It includes
an introduction to Standard ML and 3 lectures on the modules system.

Mads Tofte
Four Lectures on Standard ML
LFCS Report Series  ECS-LFCS-89-73
Laboratory for Foundations of Computer Science
Department of Computer Science
University of Edinburgh
March 1989

The following report is available from the LFCS (Lorraine Edgar,
[e-mail]) and is free.  It introduces Extended ML, a language
for writing (non-executable) specifications of Standard ML programs and
for formally developing Standard ML programs from such specifications.

Don Sannella
Formal program development in Extended ML for the working programmer.
LFCS Report Series  ECS-LFCS-89-102
Laboratory for Foundations of Computer Science
Department of Computer Science
University of Edinburgh
December 1989
--------------------------------------------------------------------------
6. Where can I find library code?

The Edinburgh SML Library provides a consistent set of functions on the
built-in types of the language and on vectors and arrays, and a few extras.
It includes a "make" system and a consistent set of parsing and unparsing
functions.  The library consists of a set of signatures with sample portable
implementations, full documentation, and implementations for Poly/ML,
Poplog ML and SML/NJ that use some of the non-standard primitives
available in those systems.  It is distributed with Poly/ML, Poplog ML and
Standard ML of New Jersey.  It is also available from the LFCS.

The library documentation is available as a technical report from the LFCS
(Lorraine Edgar, [e-mail]) and costs 5 pounds or 10 US dollars.
The LaTeX source of the report is included with the library.

Dave Berry
The Edinburgh SML Library
LFCS Report Series  ECS-LFCS-91-148
Laboratory for Foundations of Computer Science
Department of Computer Science
University of Edinburgh
April 1991


The SML/NJ Library is distributed with the SML of New Jersey compiler.
It provides a variety of utilities such as 2-dimensional arrays, sorting,
sets, dictionaries, hash tables, formatted output, Unix path name
manipulation, etc.  The library compiles under SML/NJ but should
be mostly portable to other implementations.

--------------------------------------------------------------------------
7. Theorem Provers and ML

(Collected by Paul Black, [e-mail].  Thanks Paul!)

- LCF (Edinburgh LCF and Cambridge LCF)
    * written in the original Edinburgh dialect of ML from which SML developed.

   "Logic and Computation: Interactive Proof with Cambridge LCF"
    also by Lawrence C. Paulson.


- Lego (LFCS, Edinburgh Univ., SML)
    * originally developed in CAML
    * latest version (5) now runs under SML/NJ
    * only higher-order resolution
    * available via anon. ftp from ftp.dcs.ed.ac.uk:/pub/lego

- HOL90 (Konrad Slind, TU Munich)
    * reimplementation of HOL in SML

    * freely available; ftp from Munich

    * HOL90 has lots of decision procedures, and lots of rewriting.
    In general, HOL90 has LOTS of automated support.  But it
    doesn't have dependent types (if one cares about those things).

- NuPrl (from Bob Constable`s group at Cornell)

- Isabelle (Lawrence C. Paulson, Cambridge Univ. )
    * has rewriting, but not many decision procedures.  It does has
    things like model elimination-based decision procedures.
    * a generic automatic theorem prover i.e. you can program it to
    the logic system/proof system you want.  Already has the
    following subsystems already implemented:
        i) FOL - first order logic
        ii) HOL - higher order logic
        iii) LCF - Logic of computable functions
        iv) LK - Gentzen system LK
        v) Modal - Modal logic systems T, S4, S43
        vi) ZF - Zermelo-Fraenkel set theory
    * ftp from <gannet.cl.cam.ac.uk>

- MERILL (Brian Matthews, U. of Glasgow & Rutherford Appleton Laboratory)
    * written in standard ML
    * a general purpose order-sorted equational reasoning system
    * Allows the user to declare their own object language, allows
    AC-rewriting and AC-unification of terms and equations, has
    several completion algorithms, is built on a hierarchy of
    types known as Order-Sorting, and allows the user to try
    different termination methods.
    * available via anonymous ftp from the University of Glasgow,
    ftp address: ftp.dcs.glasgow.ac.uk (130.209.240.50)
    * Brian Matthews, [e-mail] or [e-mail]

- FAUST (Karlsruhe)
    * a HOL add-on written in ML.
    * ftp from goethe.ira.uka.de (129.13.18.22)

- Alf
    * written in SML
    * only higher-order resolution

- Coq
    * written in Caml-Light (but Caml-Light and SML are VERY similar)
    * no serious automated reasoning subsystems (other than
    higher-order resolution), but has a VERY nice package for
    program verification.
    * available via anon. ftp from ftp.inria.fr:/INRIA/coq/V5.8
    * possible contact: Chet Murthy <[e-mail]>

- ICLHOL/ProofPower (ICL Secure Systems)
    * a commercial system using a reimplementation of HOL in SML
    * contact [e-mail]

- Lamdba/DIALOG (Abstract Hardware Ltd)
    * a commercial tool written in Poly/ML, neither of which is free.

- Elf (Frank Pfenning, Carnegie Mellon Univ.)
   * Elf is a higher-order logic programming language based on the LF
    Logical Framework.
   * Elf is not a theorem prover per-se, but is useful for specifying
    and proving properties of programming languages, logics, and their
    implementations.  A number of examples are provided with the
    distribution.
   * The Elf implementation is written in SML/NJ and should be easily
        portable to other SML implementations.
   * Elf can be ftp'd from alonzo.tip.cs.cmu.edu (128.2.209.194)
    in the directory /afs/cs/user/fp/public.
   * A bibliography and a collection of papers regarding LF and Elf
        can be found in the directory /afs/cs/user/fp/public/elf-papers.
   * There is an Elf mailing list.  Contact [e-mail] to join.
   * For further information, contact Frank Pfenning ([e-mail]).

References
   "ML for the Working Programmer" by Lawrence C. Paulson contains a
    small first-order theorem prover.

    Paulson also has a good chapter on writing theorem provers in ML in
    "Handbook of logic in computer science",
    Edited by:  S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum.
    Oxford : Clarendon Press, 1992-.
    CALL#: QA76 .H2785 1992


Others
    We have an automated theorm proving system here at the University
    of Tasmania, but it is still under development, currently
    riddled with bugs and has an obscure "input language"; aside
    from those minor problems, it'd be perfect...
    La Monte H. Yarroll <[e-mail]>

    Edinburgh's Concurrency Workbench and Sussex's Process Algebra
    Mauipulator are also ML systems of note, though neither are
    interactive theorem provers.


--------------------------------------------------------------------------
8. Miscellaneous

How do I write the Y combinator in SML without using a recursive
definition (i.e. "fun" or "let rec")?

    datatype 'a t = T of 'a t -> 'a

    val y = fn f => (fn (T x) => (f (fn a => x (T x) a)))
                         (T (fn (T x) => (f (fn a => x (T x) a))))

Where can I find an X-Windows interface to SML?

    Poly/ML, Poplog/ML, and SML/NJ all come with X-Windows interfaces.
    See the appropriate entries under section 3.  In addition, Poly/ML
    interfaces to the industry standard OSF/Motif toolkit.

How do I call a C function from SML/NJ?

See the file runtime/cfuns.c for example C functions that are in
the runtime and callable from ML.  You have to enter the function
into a table at the end of the file along with a string.  You use
the function System.Unsafe.CInterace to look up the function, using
the string as the key.  Note that you'll need to convert ML values
to C representations and back.  You'll have to rebuild the compiler
using makeml.

How do I get the emacs mode to work with Emacs version 19?

Add these three lines at the top of your `sml-init.el' file:
- ----- BEGIN addition
; emacs 19 doesn't have `make-shell', which sml-shell needs, so get it
; when necessary.  12 Oct 1993 M-J. Dominus ([e-mail])
(autoload 'make-shell "make-shell" "Make and initialize shell buffer for SML." nil)
- ----- END addition

They tell emacs to load the file `make-shell.el' when it needs to use
the `make-shell' function.

Then install this file as `make-shell.el' somewhere on your load path,
probably in your emacs `site-lisp' directory: